Nuprl Lemma : map_map
2,24
postcript
pdf
A
,
B
,
C
:Type,
f
:(
A
B
),
g
:(
B
C
),
as
:
A
List. map(
g
;map(
f
;
as
)) = map(
g
o
f
;
as
)
C
List
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
origin
A, B, C:Type, f:(A
B), g:(BC), as:A List. map(g;map(f;as)) = map(g o f;as) 
C List A, B, C:Type, f:(AB), g:(BC), as:A List. map(g;map(f;as)) = map(g o f;as) C List Tx:A. B(x)